X:Type, eq:EqDecider(X), f,g:fpf(X; x.Type).
fpf-sub(X; x.Type; eq; g; f)
 guard((x:X. subtype_rel(fpf-cap(f; eq; x; top); fpf-cap(g; eq; x; top)))) 

latex

Definitions	x:A. B(x), P  Q, guard(T), fpf-cap(f; eq; x; z), top, t  T, if b then t else f fi , x. t(x), tt, ff, prop{i:l}, fpf-sub(A; a.B(a); eq; f; g), , x(s), Unit, P  Q, P  Q, A c B, A, False,
Lemmas	fpf-dom wf, fpf-trivial-subtype-top, bool wf, eqtt to assert, fpf-ap wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, fpf-cap wf, top wf, fpf-sub wf, fpf wf, deq wf